T:Type, eq:EqDecider(T), L:T List, i:||L||.
no_repeats(T;L)  mu(i@0.eqof(eq)(L[i],L[i@0])) = i   

latex

Definitions	, s = t, P  Q, False, A, P & Q, AB, i  j < k, {x:A| B(x) }, {i..j}, t  T, x:A. B(x), a<b, #$n, Void, x:AB(x), l[i], P  Q, x:AB(x), b, P  Q, True, eqof(d), f(a), x.A(x), , Type, EqDecider(T), type List, no_repeats(T;l), mu(f), ||as||, (x ! l), (x  l), T, A & B, x:A. B(x)
Lemmas	no repeats member, select member, no repeats wf, deq wf, mu-bound-unique, le wf, assert wf, eqof wf, int seg wf, eqof eq btrue, deq property, select wf, length wf1